r:rationals. (1 * r) = r 

latex

Definitions	qinv(r), ff, tt, if b then t else f fi , qdiv(r; s), P  Q, t  T, P  Q, qeq(r; s), P  Q, r * s, x:A. B(x), False, nequal(T; a; b), A, A c B, int_nzero, x:A. B(x), P  Q, prop{i:l}, subtype(S; T)
Lemmas	rationals wf, qeq wf2, assert wf, assert of eq int, int nzero properties, q-elim, int inc rationals, qmul wf, assert-qeq